es:event_system{i:l}, e:es-E(es), l:IdLnk. es-receives(es; e; l)  (es-E(es) List) 

latex

Definitions

void, x:AB(x), x:A  B(x), A c B, False, A, idlnk-deq, es-eq(es), rcv-from-on(dE; dL; info; e; l; r), Type, {x:A| B(x)} , type List, subtype(S; T), receives(dE; dL; pred?; info; p; e; l), es-receives(es; e; l), EOrderAxioms(E;pred?;info), prop{i:l}, event_system{i:l}, es_info(es), es-pred?(es), es-E(es), pred!(e;e'), SWellFounded(R(x;y)), es-oaxioms(es), t.1, destination(l), loc(e), Id, s = t, e < e', P  Q, P  Q, link(e), IdLnk, P  Q, sender(e), rcv?(e), b, x:A. B(x), x:A. B(x), t  T, pred(e), first(e), a < b, , f(a)

Lemmas

rcv? wf, sender wf, nat wf, not wf, first wf, pred wf, IdLnk wf, event system wf, es-oaxioms wf, EOrderAxioms wf, es-pred!-wellfounded, receives wf, es-pred? wf, assert wf, rcv-from-on wf, es-E wf, Id wf, es-eq wf, idlnk-deq wf, es info wf